…ions

this gives a much more precise (and sound) treatment to how everything
is stitched together when combining two single-sided analysis nodes
into a two-sided node. Importantly, the "no-op" bundle for each
single sided analysis is modeled as making a no-op for the single-sided
node under consideration, but an undefined transition for the
other side of the analysis.

These undefined transitions are collected as uninterpreted functions, which
are eventually to be defined by propagating them backwards through
the single-sided analysis. Since this step is not complete, we now
expect to generate unprovable assertions which contain these functions.

…g issues

this avoids complications with grounding, which
doesn't support uninterpreted functions

this avoids edge cases where the globally-scoped value contains
fresh variables for values that should always be concrete
(e.g. registers that are necessarily bitvectors)

this is just for convenience, since every usage of 'withFreshScope'
worked around the wrapping

scopes

ensures that when a two-sided node is split, the resulting
single-sided nodes mark the original node as the divergence point

previously this was checked at run-time. With the
'Quant' module we can enforce this statically by
restricting the allowed cases for divergence points

…eturn site bundle

avoids issues with assertion propagation where the free variable
used to specify this value would escape its scope and cause
unpredictable behavior (i.e. infinite loops)

when combining single-sided nodes, the resulting
(two-sided) node should be annotated with the
initial divergence point (which must be
shared between the single-sided nodes)

this is a convention that simplifies recovering
control flow divergence information, but needs to
be consistently applied to avoid inconsistencies

adds a flag to "ProcessNode" that indicates when
additional control flow merge logic should fire when
the node is processed.

ensures that, in the case where the assertion is not
discharged, the resulting predicate fully internalizes
the two single-sided analyses (i.e. converts the
two independent assertions back into a relation)

this was causing issues where two variants of the
same node would be created (one with the divergence
point and one without)

I don't believe this is actually needed anymore, but
in the worst case we can store a reverse map in
the pairgraph to recover the original single-sided
nodes from a merged node

…o sided nodes

…stack

when defining a domain refinment (i.e. asserting/assuming
that locations are equal) there are two steps:
1) defining the set of locations
2) computing a sufficient condition to make those locations equal

these steps occur in different variable scopes, and so the bound
variables in any symbolic locations from step 1) are
re-bound to the corresponding variables during step 2)

without this step, attempting to refine a domain that contains
symbolic pointers would have no effect

…nodes

now merged sync points don't have a corresponding diverge point,
so to determine if a two-sided node is a merged sync point we
need to consult the graph

attempting to schedule a single-sided sync point should always
trigger a merge